n:. CoPrime(fib(n),fib(n+1)) 

latex

Definitions	AB, A, False, CoPrime(a,b), ij, P  Q, x:A. B(x), t  T, , i=j, T, fib(n), True, Prop, Unit, P  Q, P  Q, p  q, P  Q, , p  q, b, P & Q, b, GCD(a;b;y)
Lemmas	gcd p wf, gcd p shift, gcd p sym, assert wf, not wf, bnot wf, band wf, bool wf, eq int wf, bor wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, and functionality wrt iff, assert of band, bnot thru bor, eqff to assert, or functionality wrt iff, assert of bor, eqtt to assert, le wf, fib wf, coprime wf, true wf, squash wf, gcd p one, nat wf, nat properties, ge wf